f2(f2(a, b), x) -> f2(b, f2(a, f2(c, f2(b, f2(a, x)))))
f2(x, f2(y, z)) -> f2(f2(x, y), z)
↳ QTRS
↳ DependencyPairsProof
f2(f2(a, b), x) -> f2(b, f2(a, f2(c, f2(b, f2(a, x)))))
f2(x, f2(y, z)) -> f2(f2(x, y), z)
F2(x, f2(y, z)) -> F2(x, y)
F2(f2(a, b), x) -> F2(b, f2(a, f2(c, f2(b, f2(a, x)))))
F2(f2(a, b), x) -> F2(a, x)
F2(f2(a, b), x) -> F2(a, f2(c, f2(b, f2(a, x))))
F2(x, f2(y, z)) -> F2(f2(x, y), z)
F2(f2(a, b), x) -> F2(b, f2(a, x))
F2(f2(a, b), x) -> F2(c, f2(b, f2(a, x)))
f2(f2(a, b), x) -> f2(b, f2(a, f2(c, f2(b, f2(a, x)))))
f2(x, f2(y, z)) -> f2(f2(x, y), z)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
F2(x, f2(y, z)) -> F2(x, y)
F2(f2(a, b), x) -> F2(b, f2(a, f2(c, f2(b, f2(a, x)))))
F2(f2(a, b), x) -> F2(a, x)
F2(f2(a, b), x) -> F2(a, f2(c, f2(b, f2(a, x))))
F2(x, f2(y, z)) -> F2(f2(x, y), z)
F2(f2(a, b), x) -> F2(b, f2(a, x))
F2(f2(a, b), x) -> F2(c, f2(b, f2(a, x)))
f2(f2(a, b), x) -> f2(b, f2(a, f2(c, f2(b, f2(a, x)))))
f2(x, f2(y, z)) -> f2(f2(x, y), z)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F2(f2(a, b), x) -> F2(b, f2(a, f2(c, f2(b, f2(a, x)))))
F2(f2(a, b), x) -> F2(b, f2(a, x))
F2(f2(a, b), x) -> F2(c, f2(b, f2(a, x)))
Used ordering: Polynomial Order [17,21] with Interpretation:
F2(x, f2(y, z)) -> F2(x, y)
F2(f2(a, b), x) -> F2(a, x)
F2(f2(a, b), x) -> F2(a, f2(c, f2(b, f2(a, x))))
F2(x, f2(y, z)) -> F2(f2(x, y), z)
POL( F2(x1, x2) ) = max{0, x1 - 2}
POL( f2(x1, x2) ) = x1
POL( a ) = 3
POL( b ) = 0
POL( c ) = 0
f2(x, f2(y, z)) -> f2(f2(x, y), z)
f2(f2(a, b), x) -> f2(b, f2(a, f2(c, f2(b, f2(a, x)))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
F2(x, f2(y, z)) -> F2(x, y)
F2(f2(a, b), x) -> F2(a, f2(c, f2(b, f2(a, x))))
F2(f2(a, b), x) -> F2(a, x)
F2(x, f2(y, z)) -> F2(f2(x, y), z)
f2(f2(a, b), x) -> f2(b, f2(a, f2(c, f2(b, f2(a, x)))))
f2(x, f2(y, z)) -> f2(f2(x, y), z)